es:ES, X:AbsInterface(Top), f:(E(X)E(X)).
(x:E(X). f(x) c x)  (e:E(X). prior-f-fixedpoints(e) ~ prior-f-fixedpoints(f**(e))) 

latex

Definitions

t  T, b, {x:A| B(x)} , E(X), let x,y = A in B(x;y), t.1, x:AB(x), x:A. B(x), a:A fp B(a), strong-subtype(A;B), P  Q, ES, AbsInterface(A), e c e', x:A  B(x), left + right, P  Q, (e < e'), Top, Dec(P), (e <loc e'), e loc e' , x:A. B(x), e<e'.P(e), ee'.P(e), e<e'. P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), EState(T), Id, , Type, EqDecider(T), Unit, IdLnk, EOrderAxioms(E; pred?; info), kindcase(k; a.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', , constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,y. t(x;y), Void, x:A.B(x), S  T, suptype(S; T), first(e), A, <a, b>, pred(e), x.A(x), x. t(x), P & Q, e  X, s ~ t, f(a), E, s = t, f**(e), False, ff, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , b, tt, P  Q, p  q, p  q, p q, {T}, SQType(T), e = e'

Lemmas

bool cases, guard wf, bool sq, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-es-eq-E-2, es-eq-E wf, false wf, es-fix-sqequal, es-interface wf, es-is-interface wf, es-causl wf, es-causle wf, deq wf, EOrderAxioms wf, kind wf, Msg wf, nat wf, val-axiom wf, cless wf, qle wf, bool wf, Knd wf, kindcase wf, IdLnk wf, constant function wf, loc wf, not wf, assert wf, first wf, top wf, unit wf, pred! wf, strongwellfounded wf, rationals wf, Id wf, EState wf, event system wf, decidable es-E-equal, es-E-interface-subtype rel, member wf, es-E wf, es-E-interface wf, subtype rel wf